Nuprl Definition : es-bc
11,40
postcript
pdf
es-bc{i:l}(
es
;
e
;
e'
)
== case TERMOF{
decidable
es-causl
:ObjectId, 1:l, i:l}(
es
,
e'
,
e
) of inl(
x
) => tt | inr(
x
) => ff
latex
clarification:
es-bc{i:l}
es-bc
(
es
;
e
;
e'
)
== case TERMOF{
decidable
es-causl
:ObjectId, 1:l, i:l}(
es
,
e'
,
e
) of inl(
x
) => tt | inr(
x
) => ff
latex
Definitions
ff
,
tt
,
decidable
es-causl
,
f
(
a
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
FDL editor aliases
es-bc
origin